Papers by Andrew C Yao
Hierarchical Attention Generates Better Proofs (2025.acl-long)
Copied to clipboard
| Challenge: | Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs. |
| Approach: | They propose a regularization method that aligns LLMs’ attention mechanisms with mathematical reasoning structures and establishes a five-level hierarchy from foundational elements to high-level concepts. |
| Outcome: | The proposed method improves proof success rates by 2.05% on miniF2F and 1.69% on ProofNet while reducing proof complexity by 23.81% and 16.50% respectively. |
Autonomous Data Selection with Zero-shot Generative Classifiers for Mathematical Texts (2025.findings-acl)
Copied to clipboard
| Challenge: | Existing methods that require human annotations or training a dedicated data filter to curate high-quality mathematical texts are based on autonomous data selection. |
| Approach: | They propose a method that leverages base language models as zero-shot "generative classifiers" they use a model's logits to determine whether a given passage is mathematically informative and educational . |
| Outcome: | The proposed method significantly boosts downstream performance on math benchmarks while using far fewer tokens than previous methods. |